perm filename TA.F80[206,LSP] blob
sn#552844 filedate 1980-12-16 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00016 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 Tasks for TAing CS 206 fall quarter 1980-81 for McCarthy.
C00007 00003 The source file for LISP at LOTS is LSPLOT.F79[206,lsp]. I told JMC
C00009 00004 75 15 60 ... 100 25
C00012 00005 Homework 1. Tuesday, Oct 14, 1980.
C00014 00006 \|\\
C00027 00007 (DEFUN PARTITION (u n)
C00029 00008 \|\\
C00045 00009 page function type, number of arguments
C00048 00010 page function type, number of arguments
C00051 00011 page function type, number of arguments
C00054 00012 page function type, number of arguments
C00057 00013 union[u,v] ←
C00059 00014 Homework 3. Thursday, Oct 30, 1980.
C00072 00015 \|\\
C00084 00016 Midterm -- Nov 13, 1980
C00086 ENDMK
C⊗;
Tasks for TAing CS 206 fall quarter 1980-81 for McCarthy.
Major task: be in charge of getting the next edition of McCarthy/Talcott
pubbed and printed. What are the deadlines which must be met?
Also get a copy of the MacLisp manual.
Using Lisp at LOTS is also needed, but such handouts can be handled later.
Ask Denny Brown about getting office space.
Get accounts on LOTS and Score. Does Maclisp still work as advertised on LOTS?
Martin Brooks, now in Santa Cruz, TAed for Carolyn last go round. Talk to him.
Pump Dick Gabriel for any last minute Maclisp information before he leaves
at the end of the summer.
Ask about Gips, Stylus.
Invert LISP, McCarthy, CAR/CDR...
Yes, I will do test making and grading.
McCarthy reaffirms yes indeed he and Knuth support my being a PhD candidate,
and in fact JMC is surprised that his letter of recommendation last time
was not strong enough. So no need to worry.
The main project he would like me to work on is a super-pretty print,
which does rather arbitrary transformations of classes of formulas from
internal to external notations. E.g. doing what TEX does, except with
a meta-language so that formats can be specified for whole classes of
input. And of course with local override capabilities.
Finish FOLytopes. JMC affirms that any paper will do. Wonders why a
"repaired" graph theoretic or perhaps 2-d algebraic edge loop representation
proof doesn't exist.
My proof grows out of a number of fundamental dissatisfactions with existing
proofs of Euler's relation. Mine is more fundamental, making fewer assumptions,
serves as the basis for a theory, less geometric. It has also been refined
under the weight of an extremely rigorous if narrow-minded proof checker.
Taught me much about what is needed in constructing air-tight theories.
Further theory doesn't exist yet, but should be interesting.
Exactly where it will go is unclear; has been bothering me for a long time.
See BOOK.DIR[BOO,JMC] for the root of the tree which constitutes
Lisp: Programming and Proving.
The source file for LISP at LOTS is LSPLOT.F79[206,lsp]. I told JMC
that you may use what ever ammount of it that you want to print, just
make sure that all references to me are purged. This includes CLTs
appearing in examples etc. Please make a copy of this and
any other file you wish to modify in your own area. Also, please don't
change files in or add files to the 206,lsp area. If you have things
which you think should be kept for posterity (like problem sets and
soluution) send me a list with pointers and documentation at the
end of the quarter. I have the 206,lsp area in a semi-organized
semi-incoherent state and it will be easier to make progress if
I am the only one munging it for the time being.
75 15 60 ... 100 25
HWK1 HWK2 HWK3 MID
---- ---- ---- ---
? c partial 50 57 0 Alfaro, Joe
b-a 60 12 48 + 86 15 Autilio, Pat
a 68 3 60 + 95 21 Bradford, Ethan
? c-b 56 13 43 63 5 Costello, Peter
b-a 75 0 52 + 87 0 Costigan, Peter [PDC]
a- 51 15 28 + 91 10 Craig, John [JRC]
a 56 15 60 93 0 Davey, Mark
a ... 60 92 18 Demetrescu, Stefan (p/nc)
? b 59 15 55 + 78 0 Falis, Ed [EPF]
a 68 7 55 + 91 10 Finlayson, Ross [RSF]
b+ 58 15 60 + 84 0 Hansen, Tony
b+ 64 5 50 84 20 Hartman, Doug [DOH]
b- 63 4 60 + 72 0 Iwasaki, Yumi
? c+ 57 13 71 5 Johnson, John (p/nc)
? b- ... 77 0 Kelley, John
a 75 0 60 + 91 25 King, Jonathan [SQU]
a 70 0 60 + 95 5 Malik, Jitendra [JMM]
a 65 2 60 + 94 25 Olum, Ken [KDO]
a 58 15 54 92 25 Pehoushek, Joe
b-a 58 + 87 0 Porter, Rick
... 58 11 60 68 20 Schellentrager, Jeff (p/nc)
a- 61 9 58 + 88 3 Strauss, Randy [RAS]
a- 59 15 60 + 89 25 Taylor, Robert [RRT]
... 52 13 55 64 10 Tsang, Robert (p/nc)
a- 91 25 Wang, Peter
a 75 0 60 + 96 25 Weening, Joseph [JJW]
a 68 7 60 93 15 Yankowski, Fred [FCY]
Homework 1. Tuesday, Oct 14, 1980.
Assignment: McCarthy Talcott, pp45-46 #1-13
partial Alfaro, Joe
65 10 Altman, Stu
60 12 Autiliv, Pat
68 3 Bradford, Ethan
75 0 Costigan, Peter
56 13 Costello, Peter
51 15 Craig, John
56 15 Davey, Mark
54 15 Dehirchul, Linda
Demetrescu, Stefan
51 12 Evans, Maureen L.
59 15 Falis, Ed
68 7 Finlayson, R. S.
69 5 Greene, George R.
58 15 Hansen, Tony
64 5 Hartman, Doug
63 4 Hempel, Thomas
62 7 Iwasaki, Yumi
57 13 Johnson, John
63 10 Kanefsky, Bob
Kelley, John
75 0 King, John
70 0 Malik, Jitendra
65 2 Miller, Gary
70 4 Olum, Ken
58 15 Pehoushek, Dan
Porter, Rick
50 11 Schellentrager, Jeff
61 9 Strauss, Randy
45 15 Tani, John
59 15 Taylor, Bob
52 13 Tsang, Robert
75 0 Weening, Joseph
68 7 Yankowski, Fred
\|\\;
\M1NONLB;\;
\M2NONMB;\;
\M3NONM;\;
\M4FIX25;\;
\M5NONS;\;
\M6NONSB;\;
\C\F1Homework #1 solutions.
\C\F2Lisp: Programming and Proving\F3, page 45, problems 1-13
\CCS206 (Lisp) Fall 1980
\CThursday October 30, 1980
\CProfessor: John McCarthy
\CTA: Scott Kim
\J\F6Grading. \F55 possible points were assigned each problem, except for
problem 8, which was assigned 15 points (10 for \F6partition\F5 and 5 for
\F6testpart). I am deliberately being rather picky in grading, so don't be
bothered if I take off lots of points. The purpose is to separate the
grades as clearly as possible so I can see how people are doing. I realize
problem 8 was very difficult, so I am recording the grade for that problem
separate from the rest of the homework. The assignment was intended to be
in external notation; many people used internal. That's ok, but it is
extremely important that you know both well for the tests, so I recommend
you \F6always \F5plan your programs first in external notation.
\F6Error conditions. \F5Unless explicitly stated otherwise, you can assume
that input variables are of the proper sort (e.g. list).
\F6Recommendations. \F5Make sure you answer all the questions (e.g. even
if you didn't get \F6partition\F5, you could try \F6testpart\F5. Be very
careful of termination conditions, especially on empty cases. Be careful
to distinguish \F6cons\F5 and \F6append\F5. There is always more than one
solution: strive for concise (but clear) formulations. The problems given
in class will almost always have reasonably elegant solutions. Try to
avoid inefficient or indirect solutions, even if they work--for problems
4,5,6 many people used REVERSE. Such programs are much harder to make
proofs about. Use help functions. If you need a global variable, consider
a help function with an extra variable. Be precise. If you're testing for
NIL, use NULL, not ATOM. Use <'A> as the external notation for (LIST 'A)
or (CONS 'A NIL). Use (A . B) as the external notation for (CONS A B) (I
know that's a pun, but...). !!!!! The expression "IF condition THEN T ELSE
NIL" should be written as just "condition"!!!!!!!
\F6To think recursively. \F5The key question to ask yourself is "How can
the problem be defined in terms of the next smaller problem?". It is
\F6not\F5 helpful to imagine the entire stack of recursive calls; think
inductively. Considering special cases (e.g. the empty case) helps, so
does working through examples (especially if you get stuck).
\F6Problems with LOTS.\F5 I realize the documentation is not the best in
the world. The obscurities of editing, I/O, and so on, seem to be getting
in people's way. I would like to hold a problem session to answer questions
about LOTS (or other Lisp systems), work through the homework problems,
and answer questions about Lisp internal notation syntax.
\F6Homework solutions.\F5 I'm using uppercase instead of \F6bold\F5 or
underlined characters. Often there is more than one solution given;
preferred solution is given first. Alternate solutions are usually
less compact--they are given to show how different common patterns
can be compressed.\.
\F4
---------------------------------------------
(1) samelength[u,v] ←
IF N u OR N v THEN N u AND N v
ELSE samelength[D u,D v]
samelength[u,v] ←
IF N u THEN N v
ELSE IF N v THEN NIL
ELSE samelength[D u,D v]
---------------------------------------------
(2) prup[u,v] ←
IF N u THEN NIL
ELSE (A u . A v) . prup[D u,D v]
prup[u,v] ←
IF N u AND N v THEN NIL
ELSE IF N u OR N v THEN ERROR
ELSE (A u . A v) . prup[D u,D v]
---------------------------------------------
(3) istail[u,v] ←
(u=v) ∨ (N v) ∧ istail[u,D v]
istail[u,v] ←
IF u=v THEN T
ELSE IF N v THEN NIL
ELSE istail[u,D v]
---------------------------------------------
(4) commontail[u,v] ←
IF istail[u,v] THEN u
ELSE commontail[D u,v]
commontail[u,v] ←
IF N u THEN NIL
ELSE IF istail[u,v] THEN u
ELSE commontail[D u,v]
---------------------------------------------
(5) upto[u,v] ←
IF u=v THEN NIL
ELSE A v . upto[u,D v]
---------------------------------------------
(6) mapapp[f,u] ←
IF N u THEN NIL
ELSE f(A u) * mapapp[f,D u]
mapapp[f,u] ←
apply['append,mapcar[f,u]]
---------------------------------------------
(7) mapchoose[p,u] ←
IF N u THEN NIL
ELSE (IF p(A u) THEN <A u> ELSE NIL)
* mapchoose[p,D u]
mapchoose[p,u] ←
IF N u THEN NIL
ELSE IF p(A u) THEN
A u . mapchoose[p,D u]
ELSE mapchoose[p,D u]
---------------------------------------------
(8) partition[u,n] ←
IF n>length[u] THEN ERROR
ELSE IF n=length[u] THEN <mapcar[list,u]>
ELSE IF n=1 THEN <<u>>
ELSE mapcar[λv.(<A u>.v),partition[D u,n-1]]
* mapcar[λv.((A u.A v).Dv),partition[D u,n]]
testpart[u,v] ←
IF N v THEN T
ELSE testp[u,A v] AND testpart[u,D v]
testp[u,w] ←
u=merge[w]
merge[w] ←
IF N w THEN NIL
ELSE A w*merge[D w]
---------------------------------------------
Solution by Fred Yankowski
;;;; Provides error message
partition[u,n] ←
IF n>size[u] then '|N is too big|
ELSE PART1[u,n]
;;;; Easy cases, calls part2 if size≥2.
part1[u,n] ←
IF N u THEN NIL
ELSE IF n=1 THEN <<u>>
ELSE IF n>size[u] ∨ n=0 THEN NIL
ELSE PART2[<A u>,D u,(n-1)]
;;;; Forms all partitions with first set = w.
part2[w,x,m] ←
IF N x THEN NIL
ELSE IF m>size[x] THEN NIL
ELSE PREPEND[w,part1[x,m-1]] *
part1[u*A v,D v,m]
prepend[u,v] ← mapcar['[λx:u.x],v]
---------------------------------------------
Solution by Ken Olum
partition[u,n] ←
IF n>length[u] THEN 'ERROR
ELSE parta[NIL,NIL,u,n]
;;;; BEGLIST goes at front of every partition
;;;; returned by PARTA--it is a list of those
;;;; lists before the current position
;;;; already selected.
;;;; SELECTION is the portion of the current
;;;; list that will be the first element of a
;;;; partition;
;;;; REST is the rest of the current list.
;;;; N is how may partitions are desired.
;;;; If partition is impossible, returns NIL.
;;;;
;;;; First use the current selection and
;;;; recursively partition the rest of the
;;;; list, then try it with selection one
;;;; longer and rest one shorter and append
;;;; the results.
parta[beglist,selection,rest,n] ←
IF N rest THEN NIL
ELSE IF n=1 THEN
IF N selection THEN NIL ELSE <<REST>>
ELSE parta[beglist*<selection>,NIL,
rest,n-1]
* parta[beglist,<selection>*<A rest>,
D rest,n]
testpartition[p,u] ←
IF N p THEN T
ELSE apply['append,A p]=u
∧ testpartition[D p,u]
---------------------------------------------
(9) mirror[x] ←
IF AT x THEN x
ELSE mirror[D x] . mirror[A x]
---------------------------------------------
(10) occur[x,y] ←
IF AT y THEN x=y
ELSE occur[x,A y] OR occur[x,D y]
occur[x,y] ←
IF N y THEN NIL
EKSE IF AT y AND x=y THEN T
ELSE occur[x,A y] OR occur[x,D y]
---------------------------------------------
(11) multiplicity[x,y] ←
IF N y THEN 0
EKSE IF AT y AND x=y THEN 1
ELSE occur[x,A y] + occur[x,D y]
multiplicity[x,y] ←
IF AT y THEN (IF x=y THEN 1 ELSE 0)
ELSE occur[x,A y] + occur[x,D y]
---------------------------------------------
(12) ispath[p,x] ←
IF N p THEN T
ELSE IF ¬AT x THEN NIL
ELSE (IF A p=A x THEN ispath[D p,A x]) OR
(IF A p=D x THEN ispath[D p,D x])
ispath[p,x] ←
IF N p THEN T
ELSE IF ¬AT x THEN NIL
ELSE IF A p=A x THEN ispath[D p,A x]
ELSE ispath[D p,D x])
---------------------------------------------
(13) depth[x] ←
IF AT p THEN 0
ELSE 1 + MAX[depth[A x],depth[D x]]
(DEFUN PARTITION (u n)
(COND ((GREATERP n (LENGTH u))
ERROR )
((EQ n (LENGTH u))
(LIST (MAPCAR 'list u)) )
((EQ n 1 )
(LIST (LIST u)) )
(T (APPEND
(MAPCAR '(LAMBDA (v) (CONS (LIST (CAR u) ) v ))
(PARTITION (CDR u) (SUB1 n)) )
(MAPCAR '(LAMBDA (v) (CONS (CONS (CAR u) (CAR v)) (CDR v)))
(PARTITION (CDR u) n ) ) ))))
(DEFUN TESTPART (u v)
(COND ((NULL v) T)
(T (AND (TESTP u (CAR v))
(TESTPART u (CDR v)) ))))
(DEFUN TESTP (u w) (EQUAL u (MERGE w)))
(DEFUN MERGE (w)
(COND ((NULL w) NIL)
(T (APPEND (CAR w) (MERGE (CDR w)))) ))
(SETQ A '(A B C D))
(SETQ B '((A B) (C) (D E F)))
(SETQ C '(((A) (B C D))
((A B) (C D))
((A B C) (D)) ))
(SETQ D '((A) (B C D)))
\|\\;
\M1NONLB;\;
\M2NONMB;\;
\M3NONM;\;
\M4FIX25;\;
\M5NONS;\;
\M6NONSB;\;
\C\F1Homework #2 solutions.
\C\F2Lisp: Programming and Proving\F3, page 45, problems 10-20
\CCS206 (Lisp) Fall 1980
\CThursday December 11, 1980
\CProfessor: John McCarthy
\CTA: Scott Kim
\J\F6Grading. \F55 possible points were assigned each problem, except for
problem 20, which was assigned 10 points (5 each for 20.1/20.2 and 20.3/20.4).
\F6Homework solutions.\F5 I'm using uppercase instead of \F6bold\F5 or
underlined characters. Often there is more than one solution given;
preferred solution is given first. General comments: Most programs were
well presented and documented. Problem 15 (balancing a tree) caused
problems, since most people hadn't seen tree balancing before. Flatten
first, then rebuild in binary fashion, was the approach most people took.
It certainly works, but for the preferred tree-balancing algorithm (which
is quite tricky), see volume 3 of Knuth (Sorting and Searching). My style
of solution tends to use a lot of lambda expressions; explicitly named
help functions are in many cases more clear.\.
\F4
---------------------------------------------------------------------
(10)
occur[x,y] ←
IF AT y THEN x=y
ELSE occur[x,A y] OR occur[x,D y]
.....................................................................
(DEFUN OCCUR (X Y)
(COND ((ATOM Y) (EQUAL X Y))
(T (OR (OCCUR X (CAR Y))
(OCCUR X (CDR Y)) ))))
---------------------------------------------------------------------
(11)
multiplicity[x,y] ←
IF AT y THEN (IF x=y THEN 1 ELSE 0)
ELSE multiplicity[x,A y] + multiplicity[x,D y]
.....................................................................
(DEFUN MULTIPLICITY (X Y)
(COND ((ATOM Y) (COND ((EQ X Y) 1)
(T 0) ))
(T (PLUS (MULTIPLICITY X (CAR Y))
(MULTIPLICITY X (CDR Y)) ))))
---------------------------------------------------------------------
(12)
ispath[p,x] ←
IF N p THEN T
ELSE IF AT x THEN NIL
ELSE (IF A p=A x THEN ispath[D p,A x]) OR
(IF A p=D x THEN ispath[D p,D x])
.....................................................................
(DEFUN ISPATH (P X)
(COND ((NULL P) T)
((ATOM X) NIL)
(T (OR (AND (EQ (CAR P) 'A) (ISPATH (CDR P) (CAR X)))
(AND (EQ (CAR P) 'D) (ISPATH (CDR P) (CDR X))) ))))
---------------------------------------------------------------------
(13)
depth[x] ←
IF AT x THEN 0
ELSE 1 + MAX[depth[A x],depth[D x]]
(DEFUN DEPTH (X)
(COND ((ATOM X) 0)
(T (ADD1 (MAX (DEPTH (CAR X))
(DEPTH (CDR X)) )))))
---------------------------------------------------------------------
(14)
balanced[x] ←
IF AT x THEN T
ELSE ABS[DIFF[depth[A x],depth[D x]]] ≤ 1
AND balanced[A x] AND balanced[D x]
.....................................................................
(DEFUN LESSEQP (I J)
(OR (LESSP I J) (EQUAL I J)) )
(DEFUN BALANCED (X)
(COND ((ATOM X) T)
(T (AND (LESSEQP (ABS (- (DEPTH (CAR X)) (DEPTH (CDR X)))) 1)
(BALANCED (CAR X))
(BALANCED (CDR X)) ))))
---------------------------------------------------------------------
(15)
balance[x] ←
IF balanced[x] THEN x ELSE
balance1[x,
depth[A x],
depth[D x],
IF ¬AT[A x] THEN depth[AA x] ELSE NIL,
IF ¬AT[A x] THEN depth[DA x] ELSE NIL,
IF ¬AT[D x] THEN depth[AD x] ELSE NIL,
IF ¬AT[D x] THEN depth[DD x] ELSE NIL ]
balance1[x,d1,d2,d11,d12,d21,d22] ←
IF d1<d2-1 THEN
(IF d21<d22 THEN
balance[A x . AD x] . balance[ DD x]
ELSE balance[A x . AAD x] . balance[DAD x . DD x]
ELSE IF d2<d1-1 THEN
(IF d11<d12 THEN
balance[AA x ] . balance[ DA x . D x]
ELSE balance[AA x . ADA x] . balance[DDA x . D x]
ELSE balance[balance[A x] . balance[D x]]
.....................................................................
(DEFUN BALANCE (X)
(COND ((BALANCED X) X)
(T (BALANCE1 X
(DEPTH (CAR X))
(DEPTH (CDR X))
(COND ((NOT (ATOM (CAR X))) (DEPTH (CAAR X))) (T NIL))
(COND ((NOT (ATOM (CAR X))) (DEPTH (CDAR X))) (T NIL))
(COND ((NOT (ATOM (CDR X))) (DEPTH (CADR X))) (T NIL))
(COND ((NOT (ATOM (CDR X))) (DEPTH (CDDR X))) (T NIL)) ))))
(DEFUN BALANCE1 (X D1 D2 D11 D12 D21 D22)
(COND ((LESSP D1 (SUB1 D2))
(COND ( (LESSP D21 D22)
(CONS (BALANCE (CONS (CAR X) (CADR X)))
(BALANCE (CDDR X)) ) )
(T (CONS (BALANCE (CONS (CAR X) (CAADR X)))
(BALANCE (CONS (CDADR X)(CDDR X))) )) ))
((LESSP D2 (SUB1 D1))
(COND ( (LESSP D12 D11)
(CONS (BALANCE (CAAR X) )
(BALANCE (CONS (CDAR X) (CDR X))) ) )
(T (CONS (BALANCE (CONS (CAAR X) (CADAR X)))
(BALANCE (CONS (CDDAR X)(CDR X))) )) ))
(T (CONS (BALANCE (CAR X))
(BALANCE (CDR X)) ))
))
---------------------------------------------------------------------
(16)
get[y,p] ←
IF N p THEN y
ELSE IF A p=A THEN get[A y,D p]
ELSE IF A p=D THEN get[D y,D p]
.....................................................................
(DEFUN GET (Y P)
(COND ((NULL P) Y)
((EQ (CAR P) 'A) (GET (CAR Y) (CDR P)))
(T (GET (CDR Y) (CDR P)))
))
---------------------------------------------------------------------
(17)
point[x,y] ←
IF x=y THEN NIL
ELSE IF ¬AT y THEN
(λleftpath rightpath.
IF leftpath='NO THEN
(IF rightpath='NO THEN 'NO ELSE ('D . rightpath))
ELSE ('A . leftpath ) )
(point[x,A y],point[x,D y])
ELSE 'NO
.....................................................................
(DEFUN POINT (X Y)
(COND ((EQ X Y) NIL)
((NOT (ATOM Y))
((LAMBDA (LEFTPATH RIGHTPATH)
(COND ((EQ LEFTPATH 'NO)
(COND ((EQ RIGHTPATH 'NO) 'NO)
(T (CONS 'D RIGHTPATH)) ))
(T (CONS 'A LEFTPATH)) ))
(POINT X (CAR Y)) (POINT X (CDR Y)) ))
(T 'NO)
))
---------------------------------------------------------------------
(18)
allpoint[x,y] ←
IF x=y THEN <NIL>
ELSE IF ¬AT y THEN mapcar[λpp.('A . pp),allpoint[x,A y]] *
mapcar[λpp.('D . pp),allpoint[x,D y]]
ELSE NIL
.....................................................................
(DEFUN ALLPOINT (X Y)
(COND ((EQ X Y) (LIST NIL))
((NOT (ATOM Y))
(APPEND (MAPCAR '(LAMBDA (PP) (CONS 'A PP))
(ALLPOINT X (CAR Y)) )
(MAPCAR '(LAMBDA (PP) (CONS 'D PP))
(ALLPOINT X (CDR Y)) )))
(T NIL)
))
---------------------------------------------------------------------
(19)
commons[x] ←
removesingletons[allsubexppoint[x]]
removesingletons[x] ←
IF N x THEN NIL
ELSE (IF N DADA x THEN NIL ELSE <A x>)
* removesingletons[D x]
allsubexppoint[x] ←
mapcar[ λkey.<key,allpoint[key,x]>
makeset[allsubexp[x]] ]
makeset[u] ←
IF N u THEN NIL
ELSE ( IF NOT member[A u,D u] THEN <A u> ELSE NIL )
* makeset[D u]
allsubexp[x] ←
<x> * (IF AT x THEN NIL
ELSE allsubexp[A x]*allsubexp[D x])
.....................................................................
(DEFUN COMMONS (X)
(REMOVESINGLETONS (ALLSUBEXPPOINT X)) )
(DEFUN REMOVESINGLETONS (X)
(COND ((NULL X) NIL)
(T (APPEND (COND ((NULL (CDADAR X)) NIL)
(T (LIST (CAR X))) )
(REMOVESINGLETONS (CDR X)) ))))
(DEFUN ALLSUBEXPPOINT (X)
(MAPCAR '(LAMBDA (KEY) (LIST KEY (ALLPOINT KEY X)))
(MAKESET (ALLSUBEXP X)) ))
(DEFUN MAKESET (U)
(COND ((NULL U) NIL)
(T (APPEND (COND ((NOT (MEMBER (CAR U) (CDR U)))
(LIST (CAR U)) )
(T NIL) )
(MAKESET (CDR U)) ))))
(DEFUN ALLSUBEXP (X)
(APPEND (LIST X)
(COND ((ATOM X) NIL)
(T (APPEND (ALLSUBEXP (CAR X))
(ALLSUBEXP (CDR X)) )))))
---------------------------------------------------------------------
(20.1)
sum[u,v] ←
IF N u THEN v
ELSE IF N v THEN u
ELSE (A u + A v) . sum[D u,D v]
.....................................................................
(DEFUN SUM (U V)
(COND ((NULL U) V)
((NULL V) U)
(T (CONS (PLUS (CAR U) (CAR V))
(SUM (CDR U) (CDR V)) ))))
---------------------------------------------------------------------
(20.2)
prod[u,v]←
IF N v THEN NIL
ELSE sum[scalarprode[A u,v],
0 . prod[D u,v] ]
scalarprod[i,u] ←
mapcar[λj. TIMES[i,j], u]
.....................................................................
(DEFUN PROD (U V)
(SUM (MULTIPLE (CAR U) V)
(COND ((NULL (CDR U)) NIL)
(T (CONS 0 (SCALARPROD (CDR U) V))) )))
(DEFUN SCALARPROD (I U) (MAPCAR '(LAMBDA (J) (TIMES I J))
U ))
---------------------------------------------------------------------
(20.3)
quot[u,v]←
IF length[u]>length[v] THEN NIL
ELSE
λfirstterm.(firstterm . quot[u,dif[v,multiple[firstterm,u]]])
quotient[A v,A u]
.....................................................................
(DEFUN DIF (U V)
(COND ((NULL U) V)
((NULL V) U)
(T (CONS (DIFFERENCE (CAR U) (CAR V))
(DIF (CDR U) (CDR V)) ))))
(DEFUN QUOT (U V)
(REVERSE (QUOT1 (REVERSE U) (REVERSE V))) )
(DEFUN QUOT1 (U V)
(COND ((GREATERP (LENGTH U) (LENGTH V)) NIL)
(T ((LAMBDA (FIRSTTERM)
(CONS FIRSTTERM
(QUOT1 U (CDR (DIF V (MULTIPLE FIRSTTERM U)))) ))
(QUOTIENT (CAR V) (CAR U)) ))))
---------------------------------------------------------------------
(20.4)
rem[u,v]←
IF length[u]>length[v] THEN v
ELSE λfirstterm.(rem[u,dif[v,multiple[firstterm,u]]])
quotient[A v,A u]
.....................................................................
(DEFUN REM (U V)
(REVERSE (REM1 (REVERSE U) (REVERSE V))) )
(DEFUN REM1 (U V)
(COND ((GREATERP (LENGTH U) (LENGTH V)) V)
(T ((LAMBDA (FIRSTTERM)
(REM1 U (CDR (DIF V (MULTIPLE FIRSTTERM U)))) )
(QUOTIENT (CAR V) (CAR U)) ))))
page function type, number of arguments
---- -------- -------------------------
67 = SUBR 2 args
67 > SUBR 2 args
68 < SUBR 2 args
74 + LSUBR 0 or more args
75 1+ SUBR 1 arg
77 +$ LSUBR 0 or more args
78 1+$ SUBR 1 arg
74 - LSUBR 0 or more args
77 -$ LSUBR 0 or more args
78 1-$ SUBR 1 arg
74 * LSUBR 0 or more args
77 *$ LSUBR 0 or more args
75 / LSUBR 0 or more args
78 /$ LSUBR 0 or more args
75 \ SUBR 2 args
75 \\ SUBR 2 args
76 ↑ SUBR 2 args
78 ↑$ SUBR 2 args
69 abs SUBR 1 arg
72 add1 SUBR 1 arg
56 alphalessp SUBR 2 args
36 and FSUBR
19 append LSUBR 0 or more args
8 apply LSUBR 2 or 3 args
94 *array LSUBR 3 or more args
94 array FSUBR
95 arraydims SUBR 1 arg
14 arraycall FSUBR
12 arg SUBR 1 arg
63 args LSUBR 1 or 2 args
85 ascii SUBR 1 arg
28 assoc SUBR 2 args
29 assq SUBR 2 args
80 atan SUBR 2 args
1 atom SUBR 1 arg
1 bigp SUBR 1 arg
82 boole LSUBR 3 or more args
51 boundp SUBR 1 arg
15 car SUBR 1 arg
44 catch FSUBR
89 catenate LSUBR 0 or more args
15 cdr SUBR 1 arg
16 c...r SUBR 1 arg
10 comment FSUBR
36 cond FSUBR
16 cons SUBR 2 args
59 copysymbol SUBR 2 args
page function type, number of arguments
---- -------- -------------------------
80 cos SUBR 1 arg
34 cxr SUBR 2 args
55 defprop FSUBR
61 defun FSUBR
26 delete LSUBR 2 or 3 args
27 delq LSUBR 2 or 3 args
72 *dif SUBR 2 args
71 difference LSUBR 1 or more args
39 do FSUBR
97 dumparrays SUBR 2 args
3 eq SUBR 2 args
3 equal SUBR 2 args
47 err FSUBR
46 error LSUBR 0 to 3 args
46 errset FSUBR
7 eval LSUBR 1 or 2 args
79 exp SUBR 1 arg
87 explode SUBR 1 arg
87 explodec SUBR 1 arg
87 exploden SUBR 1 arg
72 expt SUBR 2 args
96 fillarray SUBR 2 args
69 fix SUBR 1 arg
1 fixp SUBR 1 arg
88 flatc SUBR 1 arg
87 flatsize SUBR 1 arg
69 float SUBR 1 arg
1 floatp SUBR 1 arg
84 fsc SUBR 2 args
13 funcall LSUBR 1 or more args
8 function FSUBR
9 *function FSUBR
72 gcd SUBR 2 args
59 gensym LSUBR 0 or 1 args
53 get SUBR 2 args
85 getchar SUBR 2 args
86 getcharn SUBR 2 args
53 getl SUBR 2 args
90 get←pname SUBR 1 arg
42 go FSUBR
67 greaterp LSUBR 2 or more args
70 haipart SUBR 2 args
66 haulong SUBR 1 arg
33 hunk LSUBR 0 or more args
2 hunkp SUBR 1 arg
page function type, number of arguments
---- -------- -------------------------
34 hunkp VARIABLE
34 hunksize SUBR 1 arg
69 ifix SUBR 1 arg
86 implode SUBR 1 arg
89 index SUBR 2 args
59 intern SUBR 1 arg
18 last SUBR 1 arg
18 length SUBR 1 arg
67 lessp LSUBR 2 or more args
19 list LSUBR 0 or more args
96 listarray LSUBR 1 or 2 args
13 listify SUBR 1 arg
97 loadarrays SUBR 1 arg
79 log SUBR 1 arg
83 lsh SUBR 2 args
14 lsubrcall FSUBR
90 make←atom SUBR 1 arg
34 makhunk SUBR 1 arg
86 maknam SUBR 1 arg
30 maknum SUBR 1 arg
51 makunbound SUBR 1 arg
99 map SUBR 2 or more args
99 mapatoms LSUBR 1 or 2 args
99 mapc SUBR 2 or more args
99 mapcan SUBR 2 or more args
99 mapcar SUBR 2 or more args
99 mapcon SUBR 2 or more args
99 maplist SUBR 2 or more args
68 max LSUBR 1 or more args
25 member SUBR 2 args
26 memq SUBR 2 args
68 min LSUBR 1 or more args
70 minus SUBR 1 arg
65 minusp SUBR 1 arg
30 munkam SUBR 1 arg
20 ncon LSUBR 0 or more args
17 ncons SUBR 1 arg
4 not SUBR 1 arg
21 nreconc SUBR 2 args
21 nreverse SUBR 1 arg
4 null SUBR 1 arg
2 numberp SUBR 1 arg
65 oddp SUBR 1 arg
36 or FSUBR
55 plist SUBR 1 arg
71 plus LSUBR 0 or more args
65 plusp SUBR 1 arg
57 pnget SUBR 2 args
57 pnput SUBR 2 args
38 prog FSUBR
page function type, number of arguments
---- -------- -------------------------
11 progn LSUBR 1 or more args
11 progv FSUBR
10 prog2 LSUBR 2 or more args
54 putprop SUBR 3 args
73 *quo SUBR 2 args
8 quote FSUBR
71 quotient LSUBR 1 or more args
81 random LSUBR 0 to 2 args
86 readlist SUBR 1 arg
95 *rearray LSUBR 1 or more args
72 remainder SUBR 2 args
59 remob SUBR 1 arg
55 remprop SUBR 2 args
43 return SUBR 1 arg
20 reverse SUBR 1 arg
83 rot SUBR 2 args
23 rplaca SUBR 2 args
23 rplacd SUBR 2 args
34 rplacx SUBR 3 args
56 samepnamep SUBR 2 args
29 sassoc SUBR 3 args
30 sassq SUBR 3 args
50 set SUBR 2 args
12 setarg SUBR 2 args
55 setplist SUBR 2 args
49 setq FSUBR
66 signp FSUBR
80 sin SUBR 1 arg
31 sort SUBR 2 args
32 sortcar SUBR 2 args
79 sqrt SUBR 1 arg
95 store FSUBR
89 stringlengthSUBR 1 arg
2 stringp SUBR 1 arg
24 sublis SUBR 2 args
13 subrcall FSUBR
2 subrp SUBR 1 arg
24 subst SUBR 3 args
90 substr LSUBR 2 or 3 args
72 sub1 SUBR 1 arg
27 sxhash SUBR 1 arg
1 symbolp SUBR 1 arg
50 symeval SUBR 1 arg
63 sysp SUBR 1 arg
45 throw FSUBR
71 times LSUBR 0 or more args
2 typep SUBR 1 arg
17 xcons SUBR 2 args
65 zerop SUBR 1 arg
81 zunderflow SWITCH
union[u,v] ←
IF N u THEN v
ELSE IF (A u)εv THEN D u ∪ v
ELSE A u . [D u ∪ v]
member[x,u] ←
¬N u ∧ (x=A u ∨ xεD u)
setdif[u,v] ←
IF N u THEN NIL
ELSE IF (A u)εv THEN setdif[D u,v]
ELSE A u . setdif[D u,v]
rcycle[p] ←
IF N p THEN NIL
ELSE <rac[p]> * rdc[p]
rac[p] ←
IF N p THEN NIL
ELSE IF N D p THEN A p
ELSE rac[D p]
rdc[p] ←
IF N p THEN NIL
ELSE IF N D p THEN NIL
ELSE A p . rdc[D p]
lcycle[p] ←
D p * <A p>
isperm1[p] ←
i[p,length[p]]
isp1[p,length] ←
N p ∨ [(1≤A p≤length) ∧ ¬(A p ε D p)]
compose1[p1,p2] ←
invert1[p] ←
inv1[1,p]
inv1[n,p] ←
IF n>length[p] THEN NIL
ELSE find[n,p]*inv1[n+1,p]
find[n,p] ←
IF n=A p THEN 1
ELSE 1+find[n,D p]
id1[p] ←
isperm2[p] ←
rho21[p] ←
compose2[p1,p2] ←
Homework 3. Thursday, Oct 30, 1980.
Assignment: McCarthy Talcott, p69 #2,3; p89 #1,4,5 (prove termination for 1,5)
*********************************************
(2) Prove: ∀u v: reverse[u * v] = [reverse v] * [reverse u]
Equivalently, prove: ∀u v: reverse1[u * v] = [reverse1 v] * [reverse1 u]
REVERSE1: IF N u THEN NIL ELSE [reverse1 D u]*<A u>
APPENDNIL: u * NIL = u
REVERSENIL: reverse NIL = NIL
Lemma (problem 1): ∀ u: reverse u = reverse1 u
Null case:
reverse1[NIL * v]
= reverse1[v] APPENDNIL
= reverse1[v] * NIL APPENDNIL
= reverse1[v] * reverse1[NIL] REVERSENIL
Inductive hypothesis: reverse1[D u * v] = [reverse1 v] * [reverse1 D u]
reverse1[uu * v]
= [reverse1 D (uu * v)] * <A v> REVERSE1
= [reverse1 (D uu) * v] * <A v> APPEND
= ([reverse1 v] * [reverse D uu]) * <A vu> INDUCTIVE HYPOTHESIS
= [reverse1 v] * ([reverse D uu] * <A vu>) APPENDASSOCIATIVITY
= [reverse1 v] * [reverse uu] REVERSE1
*********************************************
(3) Prove: ∀u: reverse reverse u = u
Equivalently, prove: ∀u: reverse1 reverse1 u = u
Null case:
reverse1 reverse1 NIL
= reverse1 NIL REVERSE1
= NIL REVERSE1
Inductive hypothesis: reverse1 reverse1 D u = D u
reverse1 reverse1 uu
= reverse1[[reverse1 D uu]*<A uu>] REVERSE1
= reverse<A uu> * reverse1[reverse1 D uu] Problem 2.
= reverse<A uu> * D uu INDUCTIVE HYPOTHESIS
= A uu * D uu Eval.
= uu APPEND
*********************************************
(1.1) Prove: samelength[u,reverse u]
REVERSE: IF N u THEN NIL ELSE [reverse D u]*<A u>
SAMELENGTH[u,v] ←
IF N u OR N v THEN N u AND N v
ELSE samelength[D u,D v]
Lemma: samelength[u,v] ∧ samelength[v,w] ⊃ samlength[u,w]
Null case:
samelength[NIL,NIL]
= T SAMELENGTH
Inductive hypothesis: samelength[D uu,reverse D uu]
samelength[uu,reverse uu]
= samelength[D uu,D reverse uu]
= samelength[D uu,D [[reverse D uu]*<A uu>]] Definition of REVERSE
Assume D uu = NIL
= samelength[NIL,D [NIL*<A uu>]] Assumption twice
= samelength[NIL,D <A uu>] Definition of APPEND
= samelength[NIL,NIL] Definition of LIST
= T Definition of SAMELENGTH
REVERSE: IF N u THEN NIL ELSE [reverse D u]*<A u>
Assume D uu ≠ NIL
Lemma: samelength[D reverse uu,reverse D uu]
Null case: (Assume D uu = NIL)
= samelength[D reverse uu,reverse NIL] Assumption
= samelength[D reverse uu,NIL] Def of REVERSE
= samelength[D [[reverse D uu]*<A uu>],NIL] Def of REVERSE
= samelength[D [NIL*<A uu>],NIL] Assumption
= samelength[D <A uu>,NIL] Def of APPEND
= samelength[NIL,NIL] Def of LIST
= T Def of SAMELENGTH Def of LIST
Inductive hypothesis: samelength[D reverse D uu,reverse DD uu]
= samelength[D [[reverse DD uu]* AD uu],reverse D uu] Def of REVERSE
= samelength[D [[D reverse D uu]* AD uu],reverse D uu] Inductive Hypot
= samelength[D [[D reverse D uu]* AD uu],reverse D uu] Inductive Hypot
samelength[D reverse uu,reverse D uu]
D reverse D u,reverse D reverse D reverse u
---------------------------------------------
(1.2) Prove: istail[commontail[u,v],v]
Null case:
istail[commontail[u,NIL],NIL]
= istail[NIL,NIL] Lemma
= T Def of ISTAIL
---------------------------------------------
Lemma: commontail[u,NIL] = NIL
Null case:
commontail[NIL,NIL]
= IF istail[NIL,NIL] THEN NIL ELSE Def of COMMONTAIL
commontail[D u,v]
= NIL since istail[NIL,NIL]
Inductive hypothesis: commontail[D u,NIL]
commontail[u,NIL]
= IF istail[u,NIL] THEN u
ELSE commontail[D u,NIL] Def of COMMONTAIL
= IF u=NIL THEN NIL
ELSE commontail[D u,NIL] Def of ISTAIL
= IF u=NIL THEN NIL ELSE NIL Inductive hypothesis
= NIL
---------------------------------------------
(1.3) Prove: istail[commontail[u,v],u]
---------------------------------------------
(1.4) Prove: commontail[u,v]=commontail[v,u]
istail[u,v] ←
(u=v) ∨ ¬(N v)∧istail[u,D v]
commontail[u,v] ←
IF istail[u,v] THEN u
ELSE commontail[D u,v]
Null case:
commontail[u,NIL]
= NIL Lemma, 1.2
commontail[NIL,u]
= IF istail[NIL,u] THEN NIL
ELSE commontail[D NIL,u] Def of COMMONTAIL
= NIL Lemma 1.4
Inductive hypothesis: commontail[D uu,v]=commontail[v,D uu]
commontail[uu,v]
= IF istail[uu,v] THEN uu
ELSE commontail[D uu,v]
= IF (uu=v) ∨ ¬(N v)∧istail[u,D v]
= IF (uu=v) ∨ istail[v,D uu]
ELSE commontail[D uu,v] Nonempty list
= IF (v=uu) ∨ ¬(N uu)∧istail[v,D uu]
ELSE commontail[D uu,v] Nonempty list, = commute
= IF istail[v,uu] THEN v
ELSE commontail[D uu,v] Def of ISTAIL
= IF istail[v,uu] THEN v
ELSE commontail[v,D uu] Inductive hypothesis
= commontail[v,uu] Def of COMMONTAIL
---------------------------------------------
Lemma: istail[NIL,v]
---------------------------------------------
(1.5) Prove: append[upto[commontail[u,v],v],commontail[u,v]]=v]
---------------------------------------------
(1.6) Prove: append[upto[commontail[u,v],u],commontail[u,v]]=u]
*********************************************
union[u,v] ←
IF N u THEN v
ELSE IF (A u)εv THEN D u ∪ v
ELSE A u . [D u ∪ v]
member[x,u] ←
¬N u ∧ (x=A u ∨ xεD u)
setdif[u,v] ←
IF N u THEN NIL
ELSE IF (A u)εv THEN setdif[D u,v]
ELSE A u . setdif[D u,v]
---------------------------------------------
(4.1) Prove: xε[u∪v] ⊃ xεu ∨ xεv
Null case.
xε[NIL∪v]
= xεv Def of UNION
= [xεu] ∨ [xεv] OR introduction. (Tautology)
Inductive hypothesis: xε[D u ∪ v] ⊃ xε[D u] ∨ xεv
xε[uu∪v]
= xε[IF (A uu)εv THEN D uu ∪ v
ELSE A uu . [D uu ∪ v]] Def of UNION
= IF (A uu)εv THEN xε[D uu ∪ v]
ELSE xε[A uu . [D uu ∪ v]] IF-THEN-ELSE distribution
= xε[D uu ∪ v] ∨ xε[A uu . [D uu ∪ v]] Tautology
= xε[D uu] ∨ xεv ∨ xε[A uu . [D uu ∪ v]] Inductive hypothesis
= xε[D uu] ∨ xεv ∨ x=[A uu] ∨ xε[D uu ∪ v]] Def of MEMBER
= xε[D uu] ∨ xεv ∨ x=[A uu] ∨ xε[D uu] ∨ xεv Inductive hypothesis
= x=[A uu] ∨ xε[D uu] ∨ xεv Tautology
= xεuu ∨ xεv Def of MEMBER
---------------------------------------------
(4.2) Prove: [xεu] ⊃ ¬xε[v-u]
*********************************************
LCYCLE:
RCYCLE:
ISPERM1:
COMPOSE1:
invert1[p] ←
inv1[1,p]
inv1[n,p] ←
IF n>length[p] THEN NIL
ELSE find[n,p]*inv1[n+1,p]
find[n,p] ←
IF n=A p THEN 1
ELSE 1+find[n,D p]
ID1:
ISPERM2:
RHO21
COMPOSE2
IF N p THEN NIL
ELSE <rac[p]> * rdc[p]
rac[p] ←
IF N p THEN NIL
ELSE IF N D p THEN A p
ELSE rac[D p]
rdc[p] ←
IF N p THEN NIL
ELSE IF N D p THEN NIL
ELSE A p . rdc[D p]
rcycle[p] ←
reverse lcycle reverse p
lcycle[p] ←
IF N p THEN NIL
ELSE D p * <A p>
(5.1) Prove: lcycle rcycle u = u
Null case:
lcycle rcycle NIL
= lcycle NIL
= NIL
lcycle rcycle uu
= lcycle [<rac[p]> * rdc[p]]
=
---------------------------------------------
(5.2) Prove: isperm1 u ⊃ [compose1[p,invert1[p]] = id1
---------------------------------------------
(5.3) Prove: isperm1 u ⊃ (compose1[invert1[p],p] = id1
---------------------------------------------
(5.4) Prove: isperm1u ⊃ [invert1 invert1 p = p]
invert1[p] ←
inv1[1,p]
inv1[n,p] ←
IF n>length[p] THEN NIL
ELSE find[n,p]*inv1[n+1,p]
find[n,p] ←
IF n=A p THEN 1
ELSE 1+find[n,D p]
isperm1[p] ←
i[p,length[p]]
isp1[p,length] ←
N p ∨ [(1≤A p≤length) ∧ ¬(A p ε D p)]
Null case:
invert1 invert1 NIL
= inv1[1,inv1[1,NIL]] Definition INVERT1
= NIL Definition of INV1, LENGTH
Inductive Hypothesis: invert1 invert1 [D pp] = D pp
invert1 invert1 pp
= inv1[1,inv1[1,pp]] Def of INVERT1
= inv1[1,find[1,p]*inv1[2,p]] Def of INV1, LENGTH
= find[1,find[1,p]*inv1[2,p]]
*inv1[2,find[1,p]*inv1[2,p]]
=
---------------------------------------------
(5.5) Prove: isperm2 u ∧ isperm2 v ⊃ rho21[compose2[u,v]] =
compose1[rho21 u,rho21 v]
\|\\;
\M1NONLB;\;
\M2NONMB;\;
\M3NONM;\;
\M4FIX25;\;
\M5NONM;\;
\M6NONMB;\;
\C\F1Midterm solutions.
\CCS206 (Lisp) Fall 1980
\CThursday November 20, 1980
\CProfessor: John McCarthy
\CTA: Scott Kim
\J\F6Grading. \F5 The test turned out to be long, so I decided to count
the last problem as extra credit which was recorded separately from the
first four problems. All problems were weighted 25 points, for a total of
100 + 25extra points. This scheme intentionally inflates the value of the
easier problems. I realize that there are some genuine uncertainties
about just how much to put down in a proof, so I weighted correct approach
more than details.\.
\F4
points number problem
------ ------ -------
10 1a Program least[u].
15 1b Program least1[x].
5 2a Program flip2[u].
20 2b Prove flip2 flip2 u=u.
20 3a Prove member[x,u] ⊃ nth[u,index[u,x]] = x.
5 3b What conditions need to be added to prove index[u,nth[u,k]]=k?
25 4 Program transpose[u].
25 5 Program linus[u].
\J\F5As a rough guage of letter grade, consider the following:\.
\F4 90- A
75-89 B
60-74 C
\J\F5but don't take low absolute scores on this test too literally. The final
and/or project will count more. Here was the grade distribution:\.
\F4 25
Scores for 25
problem 5, 5 15 25 10 0 20
for a given 25 21 25 9 18 10 20 3 0 15 0 0 0 0 5 20 10 5 0
total on --------------------------------------------------------
problems 1-4 96 95 94 93 92 91 89 88 87 86 84 78 77 72 71 68 64 63 57
-------------------------------------------------------------------------
\C\F1Solutions.
\F5Many of the solutions showed basic problems with list structure operations,
especially CONS vs. APPEND.
Five rather picky points which were frequently missed:
[1] Rank induction is needed in problem 2 (PHI(DD u) ⊃ PHI(u) is NOT list
induction, even though it is closely related).
[2] Problem 3 requires a lemma to show that the INDEX function always
returns a value ≥ 1. The proof is almost trivial, but it important to
realize at least that a proof is needed.
[3] In problem 3b, which no one got completely correct, we need both that
k≤length[u] (so that nth does not return an error) and that nth[u,k] is the
first occurrance of that element in u (so that index returns the right value).
[4] Depending on your approach to problem 4, TRANSPOSE may have required a
check for the condition N A u, which occurs when you take the MAPCAR[CDR,u]
of a single-column matrix u.
[5] LINUS[NIL] should return <1>. (I didn't count off for this omission).
\F4-------------------------------------------------------------------------
1a.
least[u] ←
IF N D u THEN A u
ELSE min[A u,least[D u]]
-------------------------------------------------------------------------
1b.
least1[x] ←
IF AT x THEN x
ELSE min[least1[A x],least1[D x]]
-------------------------------------------------------------------------
2a.
flip2[u] ←
IF N u ∨ N D u THEN u
ELSE (AD u . (A u . flip2[DD u])
-------------------------------------------------------------------------
2b.
Prove: ∀u.[flip2 flip2 u = u]
Method: Rank induction on u, where RANK[u]=length[u]
Inductive hypothesis: ∀v.[RANK[v]<RANK[u] ⊃ flip2 flip2 v = v]
Proof:
Assume N u ∨ N D u
flip2 flip2 u =
flip2 u = u Def of flip2 (first case)
Assume ¬(N u ∨ N D u)
flip2 flip2 u =
= flip2 AD u . (A u . flip2[DD u]) Def of flip2 (second case)
= A u . (AD u . flip2[DD u]) Def of flip2 (second case)
and facts about . A D
= (A u . AD u) . u Inductive hypothesis plus lemma:
length[DD u]<length[D u]<length[u]
= u Facts about . A D
-------------------------------------------------------------------------
3a.
Given: nth[u,n] ←
IF n equal 1 THEN A u ELSE nth[D u, n-1]
index[u,x] ←
IF x equal A u THEN 1 ELSE 1 + index[D u, x]
member[x,u] ←
IF ¬(N u) THEN x=A u ∨ IF ¬(N D u) THEN member[x,D u] ELSE false
Prove: ∀x u.[member[x,u] ⊃ nth[u,index[u,x]] = x]
Method: List induction on u.
Inductive assumption: member[x,D u] ⊃ nth[D u,index[D u,x]] = x
Assume member[x,u]
Case 1: x=A u
nth[u,index[u,x]]
= nth[u,1] Def of index
= A u Def of nth
= x Assumption
Case 2: ¬(x=A u).
First, note that since member[x,u] and ¬(x=A u), we have ¬(N D u) and
member[x,D u] by the definition of member.
nth[u,index[u,x]]
= nth[u, 1+index[D u,x]] Def of index.
= nth[D u,1+index[D u,x]-1] Def of nth, lemma 1, fact
that a<b ⊃ ¬(a=b)
= nth[D u,index[D u,x]] Arithmetic
= x Inductive hypothesis, fact
that member[x,D u]
-------------------------------------------------------------------------
Lemma 1:
Prove: member[x,u] ⊃ index[x,u]≥1
Method: List induction on u.
Inductive assumption: member[x,D u] ⊃ index[x,D u]≥1
Assume member[x,u]
Assume x=A u.
index[x,u]
= 1 Def of index.
≥ 1 Def of ≥
Assume member[x,u]
Assume ¬(x=A u)
Therefore ¬(N D u) and member[x,D u]
index[x,u]
1 + index[D u,x] Def of index.
≥ 1 Def of + and ≥
-------------------------------------------------------------------------
3b.
1≤k≤length[u]
and ∀j.[j<k ⊃ ¬(index[u,j]=index[u,k])]
-------------------------------------------------------------------------
4.
transpose[u] ←
IF N u ∨ N D u THEN NIL
ELSE getcolumn[u] . transpose[leavecolumn[u]]
getcolumn[u]
IF N u THEN NIL
ELSE AA u . getcolumn[D u]
leavecolumn[u]
IF N u THEN NIL
ELSE DA u . getcolumn[D u]
-------------------------------------------------------------------------
Solution by Peter Costigan:
transpose[u] ←
t1[NIL,u,NIL]
t1[u,v,w] ←
IF N u THEN (IF v THEN w
ELSE w.t1[v,NIL,NIL])
ELSE t1[D u,v*<DA u>,w*<AA u>]
-------------------------------------------------------------------------
Solution by John Kelley
transpose[u] ←
IF N u THEN u
ELSE sort[A u,transpose[D u]]
sort[u,v] ←
IF N u THEN u
ELSE <<<A u>*A v>,sort[D u,D v]>
-------------------------------------------------------------------------
Solution by Ken Olum
transpose[u] ←
IF N u ∨ N A u THEN NIL
ELSE mapcar['A,u].transpose[mapcar['D,u]]
-------------------------------------------------------------------------
5.
linus[u] ←
best[patterns[u,1]] . u
best[u] ←
IF N D u THEN A u
ELSE best[D u]
patterns[u,n] ←
IF 2*n > length u THEN NIL
ELSE [λnext.(IF next=1 THEN <0> ELSE
IF next=0 THEN <1> ELSE NIL] {threat[u,n]}
* patterns[u,n+1]
threat[u,n] ←
IF firstn[u,n-1] equal firstn[skip[u,n],n-1] THEN A skip[u,n-1]
firstn[u,n] ←
IF n=0 THEN NIL ELSE A u . firstn[D u,n-1]
skip[u,n] ←
IF n=0 THEN u ELSE skip[D u,n-1]
-------------------------------------------------------------------------
Solution modified from Stefan Demetrescu and Patrick Autilio
linus[u] ←
(λa,b: IF length[longest[a]]>length[longest(b]] THEN b ELSE a)
[1.u,0.u]
longest[u] ←
checkheads[A u,D u]
checkheads[u,v] ←
IF length[u]>length[v] THEN NIL
ELSE (λlonger. IF ¬N longer THEN longer
ELSE IF ishead[u,v] THEN u ELSE NIL)
checkheads[u*A v,D v]
ishead[u,v] ←
N u ∨ (A u=A v ∧ ishead[D u,D v])
Midterm -- Nov 13, 1980
1 2 3 4 5 Total Name
- - - - - ----- ----
24 13 0 20 0 57 Alfaro, Joe
Dropped. Altman, Stu
25 22 17 22 15 86 Autilio, Pat
25 25 23 22 21 95 Bradford, Ethan
20 18 0 25 10 68 Costello, Peter
25 24 18 20 0 87 Costigan, Peter
25 16 25 25 10 91 Craig, John
25 23 22 23 0 93 Davey, Mark
25 25 20 22 18 92 Demetrescu, Stefan
25 20 8 25 0 78 Falis, Ed
25 21 23 22 10 91 Finlayson, Ross
20 22 20 22 0 84 Hansen, Tony
25 22 12 25 20 84 Hartman, Doug
25 22 3 22 0 72 Iwasaki, Yumi
23 20 7 21 5 71 Johnson, John
21 17 15 24 0 77 Kelley, John
25 22 19 25 25 91 King, Jonathan
25 25 20 25 5 95 Malik, Jitendra
25 25 19 25 25 94 Olum, Ken
25 22 23 22 25 92 Pehoushek, Joe
0 87 Porter, Rick
20 68 Schellentrager, Jeff
3 88 Strauss, Randy
20 89 Taylor, Robert
10 64 Tsang, Robert
25 91 Wang, Peter
25 96 Weening, Joseph
15 93 Yankowski, Fred
99
98
97
96 25
95 21 5
94 25
93 0 15
92 18 25
91 10 10 25 25
90
89 20
88 3
87 0 0
86 15
85
84 0 20
83
82
81
80
79
78 0
77 0
76
75
74
73
72 0
71 5
70
69
68 20
67
66
65
64 10
63 5
62
61
60
57 0